Nuprl Lemma : divisor_of_minus
2,24
postcript
pdf
a
,
b
:
.
a
|
b
a
| -
b
latex
Definitions
b
|
a
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
t
T
,
Prop
origin
a, b:
. a | b 
a | -b a, b:. a | b a | -b x:A. B(x) Q
x:A. B(x)
T